Nuprl Definition : es-seq
0,22
postcript
pdf
es-seq(
es
;
S
) ==
e1
,
e2
:E.
e1
before
e2
S
(
e2
<
e1
)
latex
clarification:
es-seq(
es
;
S
)
==
e1
:es-E(
es
),
e2
:es-E(
es
).
e1
before
e2
S
es-E(
es
)
es-causl(
es
;
e2
;
e1
)
latex
Definitions
x
:
A
.
B
(
x
)
,
P
Q
,
x
before
y
l
,
E
,
A
,
(
e
<
e'
)
FDL editor aliases
es-seq
origin